Nuprl Lemma : no_repeats-merge
11,40
postcript
pdf
T
:Type.
subtype_rel(
T
;
)
(
bs
,
as
:(
T
List). no_repeats(
T
;
as
)
sorted(
as
)
no_repeats(
T
; merge(
as
;
bs
)))
latex
Definitions
no_repeats(
T
;
l
)
,
x
:
A
.
B
(
x
)
,
sorted(
L
)
,
t
T
,
P
Q
,
merge(
as
;
bs
)
,
subtype(
S
;
T
)
Lemmas
sorted-merge
,
sorted
wf
,
no
repeats
wf
,
s-insert-no-repeats
,
merge
wf
origin
T:Type.
)
(bs,as:(T List). no_repeats(T; as) sorted(as) no_repeats(T; merge(as; bs))) T:Type.
)
(bs,as:(T List). no_repeats(T; as) sorted(as) no_repeats(T; merge(as; bs))) x:A. B(x)
T Q